\begin{tabbing}
f2f+{-}event($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=[$e$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$]\+
\\[0ex]$\vee$ [$e$: ${\it sndr}$ $\leftarrow$is\_ack $--$ ${\it rcvr}$]
\\[0ex]$\vee$ [$e$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$]
\\[0ex]$\vee$ [$e$: ${\it rcvr}$ $\leftarrow$is\_req  $--$ ${\it sndr}$]
\-
\end{tabbing}